$\forall$$A$, $B$:Type, $x$:$A$, $v$:$B$, ${\it eqa}$:EqDecider($A$). $x$ : $v$ $\in$ $a$:$A$ fp$\rightarrow$ $x$ : $B$($a$)?Top